Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar4/secret2005SLASHcime2.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

CIRC₂(circ₂(s, t), u) -> CIRC₂(s, circ₂(t, u))
CIRC₂(cons₂(a, s), t) -> MSUBST₂(a, t)
MSUBST₂(msubst₂(a, s), t) -> MSUBST₂(a, circ₂(s, t))
CIRC₂(circ₂(s, t), u) -> CIRC₂(t, u)
CIRC₂(cons₂(lift, s), cons₂(a, t)) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(s, t)
CIRC₂(cons₂(a, s), t) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(cons₂(lift, circ₂(s, t)), u)
MSUBST₂(msubst₂(a, s), t) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), cons₂(lift, t)) -> CIRC₂(s, t)

The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CIRC₂(circ₂(s, t), u) -> CIRC₂(s, circ₂(t, u))
CIRC₂(cons₂(a, s), t) -> MSUBST₂(a, t)
MSUBST₂(msubst₂(a, s), t) -> MSUBST₂(a, circ₂(s, t))
CIRC₂(circ₂(s, t), u) -> CIRC₂(t, u)
CIRC₂(cons₂(lift, s), cons₂(a, t)) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(s, t)
CIRC₂(cons₂(a, s), t) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(cons₂(lift, circ₂(s, t)), u)
MSUBST₂(msubst₂(a, s), t) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), cons₂(lift, t)) -> CIRC₂(s, t)

The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.